T:Type, P,Q:((T List)prop{i:l}), L:(T List).
(star-append(T; P; Q)(L))
 ((Q(L))  (L1,L2:T List. ((L = append(L1; L2))  (P(L1))  (star-append(T; P; Q)(L2))))) 

latex

Definitions	P  Q, x:A. B(x), t  T, prop{i:l}, x:A. B(x), concat(ll), append(as; bs), x. t(x), l_all(L; T; x.P(x)), P  Q, P  Q, P  Q, P  Q, star-append(T; P; Q), guard(T)
Lemmas	l all nil, append assoc, l all cons, l all wf, append wf, concat wf